Theorem vtoclbg 3569

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.)

Hypotheses

Ref	Expression
vtoclbg.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
vtoclbg.2	⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
vtoclbg.3	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
vtoclbg	⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Distinct variable groups:   𝑥,𝐴   𝜒,𝑥   𝜃,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝑉(𝑥)

Proof of Theorem vtoclbg

Step	Hyp	Ref	Expression
1		vtoclbg.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
2		vtoclbg.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
3	1, 2	bibi12d 345	. 2 ⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ 𝜃)))
4		vtoclbg.3	. 2 ⊢ (𝜑 ↔ 𝜓)
5	3, 4	vtoclg 3566	1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-clel 2819

This theorem is referenced by:  alexeqg  3664  pm13.183  3679  elab6g  3682  elabgw  3692  sbc8g  3812  sbc2or  3813  sbccow  3827  sbcco  3830  sbc5ALT  3833  sbcie2g  3847  eqsbc1  3854  sbcng  3855  sbcimg  3856  sbcan  3857  sbcor  3858  sbcbig  3859  sbcal  3868  sbcex2  3869  sbcel1v  3875  sbcreu  3898  csbiebg  3954  sbcel12  4434  sbceqg  4435  csbie2df  4466  preq12bg  4878  elintrabg  4985  sbcbr123  5220  inisegn0  6128  fsn2g  7172  funfvima3  7273  elixpsn  8995  ixpsnf1o  8996  domeng  9022  1sdomOLD  9312  rankcf  10846  eldm3  35723  elima4  35739  brsset  35853  brbigcup  35862  elfix2  35868  elfunsg  35880  elsingles  35882  funpartlem  35906  ellines  36116  elhf2g  36140  bj-elpwgALT  37020  cover2g  37676  sbcrexgOLD  42741