Theorem vtoclbg 3526

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 3523	1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-clel 2804

This theorem is referenced by:  alexeqg  3620  pm13.183  3635  elab6g  3638  elabgw  3647  sbc8g  3764  sbc2or  3765  sbccow  3779  sbcco  3782  sbc5ALT  3785  sbcie2g  3797  eqsbc1  3803  sbcng  3804  sbcimg  3805  sbcan  3806  sbcor  3807  sbcbig  3808  sbcal  3816  sbcex2  3817  sbcel1v  3822  sbcreu  3842  csbiebg  3897  sbcel12  4377  sbceqg  4378  csbie2df  4409  preq12bg  4820  elintrabg  4928  sbcbr123  5164  inisegn0  6072  fsn2g  7113  funfvima3  7213  elixpsn  8913  ixpsnf1o  8914  domeng  8937  1sdomOLD  9203  rankcf  10737  eldm3  35755  elima4  35770  brsset  35884  brbigcup  35893  elfix2  35899  elfunsg  35911  elsingles  35913  funpartlem  35937  ellines  36147  elhf2g  36171  bj-elpwgALT  37049  cover2g  37717  sbcrexgOLD  42780